A:Type, eq:EqDecider(A), B:(AType), f, g, h:a:A fp B(a). h || f  h || g  h || f  g 

latex

Definitions	P  Q, False, f  g, Top, P  Q, f(x), Unit, P  Q, x  dom(f), , Prop, b, A, P & Q, b, P  Q, a:A fp B(a), x. t(x), x(s), EqDecider(T), t  T, f || g, x:A. B(x)
Lemmas	deq wf, fpf wf, fpf-compatible wf, assert wf, not wf, bnot wf, bool wf, fpf-dom wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, fpf-ap wf, fpf-join-ap, fpf-trivial-subtype-top, top wf, fpf-join wf, fpf-join-dom